package var.satisfiability.rules;

import java.util.HashSet;
import java.util.Iterator;
import java.util.Set;

import tr.edu.ege.kipler.satisfiability.UnsatisfiableException;
import tr.edu.ege.kipler.satisfiability.completion.rules.CompletionRule;
import tr.edu.ege.kipler.satisfiability.completion.rules.RuleLogger;
import tr.edu.ege.kipler.satisfiability.container.Individual;
import tr.edu.ege.kipler.satisfiability.container.World;
import tr.edu.ege.kipler.satisfiability.container.WorldConstraintSystem;
import tr.edu.ege.kipler.syntax.Name;
import tr.edu.ege.kipler.syntax.atomicformula.ConceptAssertion;
import tr.edu.ege.kipler.syntax.concept.ConceptName;


public class ConstantDomainRule extends CompletionRule {

	private boolean applied;

	public ConstantDomainRule() {
		super();
	}

	public ConstantDomainRule(WorldConstraintSystem wcs, World world) {
		super(wcs, world);
	}

	public boolean isApplied() {
		return applied;
	}

	@Override
	public void apply() throws UnsatisfiableException {
		applied = false;
		for (Name indvName : getAllIndividuals()) {
			for (World world : getWcs().getAllWorlds()) {
				ConceptAssertion ca = new ConceptAssertion(
						ConceptName.topConcept(), indvName.toString());
				if (!world.getABox().contains(ca)) {
					world.getABox().add(ca);
					applied = true;
					RuleLogger.getInstance().info(
							"WCS " + getWcs().getId()
									+ " Constant domain rule: Adding " + ca
									+ " to " + world.getName());
				}
			}
		}
	}

	public Set<Name> getAllIndividuals() {
		Set<Name> allIndividuals = new HashSet<Name>();
		for (World world : getWcs().getAllWorlds()) {
			for (Iterator<Individual> i = world.getABox().individualIterator(); i
					.hasNext();) {
				Individual indv = i.next();
				allIndividuals.add(indv.getKey());
			}
		}
		return allIndividuals;
	}
}
